package alloy.symm;

import java.util.Iterator;

import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.BinaryFormula;
import alloy.ast.Expr;
import alloy.ast.Formula;
import alloy.ast.FormulaSeq;
import alloy.ast.LogicOp;
import alloy.ast.Node;
import alloy.ast.SigExpr;
import alloy.ast.VariableExpr;

/**
 * Base class for visitors that find all relations constrained in a given way, e.g.
 * to be a {@linkplain DAGDetector_V DAG} or a {@linkplain SingletonSetDetector_V singleton set},
 * by a top-level conjunction.  Finding these may let us do special-case symmetry-breaking.
 * Alloy doesn't have syntactic features to e.g. mark a relation as a DAG, in order to keep
 * the language small and uniform; but we can still reliably/conservatively identify relations
 * constrained to be DAGs or other special-case relations, by pattern-matching on the
 * constraints of the translatable AST.
 * <p>
 * This visitor visits {@link Formula}s that are conjoined at the top level.
 */
abstract class TopLevelConjVisitor extends ASTDepthFirstVisitor {
    /////////////
    // Methods //
    /////////////

    
    public void visit(Node node_) {
	// do nothing if it's not one of the specific node types we handle explicitly
	// in particular, don't visit the children.
    }
    
    public void visit(BinaryFormula binaryFormula_) {
	if (binaryFormula_.getOp().equals(LogicOp.AND)) {
	    binaryFormula_.getLeft().applyVisitor(this);
	    binaryFormula_.getRight().applyVisitor(this);
	}
    }

    public void visit(FormulaSeq formulaSeq_) {
	for (Iterator formulaIter = formulaSeq_.getFormulas().getFormulaIter();
	     formulaIter.hasNext();) {
	    Formula formula = (Formula)formulaIter.next();
	    formula.applyVisitor(this);
	}
    }

    /** Utility routine: test if an {@link Expr} represents a relation. */
    protected static boolean _isRelation(Expr expr_) {
	return (expr_ instanceof VariableExpr && ((VariableExpr)expr_).isQuantified) ||
	    expr_ instanceof SigExpr;
    }
    
    /** Utility routine: test if an {@link Expr} is unary. */
    protected static boolean _isUnary(Expr expr_) {
	return expr_.getType().toRelationType().numBasicTypes()==1;
    }
}
